Bounded Model Checking in Practice: CBMC vs. ESBMC

Seminar

Verifying real-world programs often requires bounded approaches to make analysis tractable. Bounded Model Checking (BMC) is one such technique, used to find bugs or verify properties within finite bounds.

This topic compares two tools for BMC of C programs: CBMC and ESBMC. While CBMC is a widely used and mature verifier based on SAT/SMT solving, ESBMC is a modern alternative. The latter emphasizes support for concurrency, floating-point reasoning, and integration with different solvers. The seminar will examine their design goals, analysis strategies, expressivity, typical use cases and the practical verification experience. Students will apply both tools to a shared verification problem and compare their capabilities in practice.

Starting Points: